r:Rng, a:|r|. (a +r 0) = a & (0 +r a) = a 

latex

Up	rings 1
Definitions of Statement	Rng, r+gp
Definitions	t  T, IMonoid, x f y, P & Q, x:A. B(x), t.2, t.1, , Mon, Group{i}, r+gp, e, *, |g|
Lemmas	rng wf, grp wf, grp id wf, grp op wf, grp car wf, monoid p wf, add grp of rng wf a, mon ident